Inference at * 1 0 
Iof proof for Lemma zip wf:

.....subterm..... T:t2:n

1. T1 : Type
2. T2 : Type
3. T1 List
4. u : T1
5. v : T1 List
6. bs:(T2 List). zip(v;bs)  ((:T1  T2) List)
7. T2 List
8. T2
9. v1 : T2 List
10. rec-case(v1) of [] => [] | b::bs' => .[<u, b> / zip(v;bs')]  ((:T1  T2) List)
  zip(v;v1)  ((:T1  T2) List) 

latex

 by DupHyp (6) 
 THEN (GuardBody (-1) 
 THEN InstGenHypByAddr (-1) [] [!ml_var(bs), v1]) THENA (Auto') 
 THEN ml_nth_hyp((-1)) 

latex

 .

Definitions

f(a), <a, b>, [car / cdr], [], rec-case(a) of [] => s | x::y => z.t(x;y;z), zip(as;bs), x:A  B(x), Type, x:AB(x), type List, s = t, {T}, x:A. B(x), t  T, first  THEN second {FDLNOr8752}, !two_place_expr{$left,$middle,$right}(first;second)  {FDLNOr8753}, !ml_var(v)  {FDLNOr8893}, ml_nth_hyp(i)  {FDLNOr8894}, !one_place_expr{$left,$right}(first)  {FDLNOr8895}